0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 16 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 13 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPQMonotonicMRRProof (⇔, 150 ms)
↳20 QDP
↳21 DependencyGraphProof (⇔, 0 ms)
↳22 TRUE
transpose_in_ag(A, B) → U1_ag(A, B, transpose_aux_in_agg(A, [], B))
transpose_aux_in_agg(.(R, Rs), X1, .(C, Cs)) → U2_agg(R, Rs, X1, C, Cs, row2col_in_agaa(R, .(C, Cs), Cols1, Accm))
row2col_in_agaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_agaa(Xs, Cols, Cols1, As))
row2col_in_agaa([], [], [], []) → row2col_out_agaa([], [], [], [])
U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_agaa(Xs, Cols, Cols1, As)) → row2col_out_agaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As))
U2_agg(R, Rs, X1, C, Cs, row2col_out_agaa(R, .(C, Cs), Cols1, Accm)) → U3_agg(R, Rs, X1, C, Cs, transpose_aux_in_agg(Rs, Accm, Cols1))
transpose_aux_in_agg([], X, X) → transpose_aux_out_agg([], X, X)
U3_agg(R, Rs, X1, C, Cs, transpose_aux_out_agg(Rs, Accm, Cols1)) → transpose_aux_out_agg(.(R, Rs), X1, .(C, Cs))
U1_ag(A, B, transpose_aux_out_agg(A, [], B)) → transpose_out_ag(A, B)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
transpose_in_ag(A, B) → U1_ag(A, B, transpose_aux_in_agg(A, [], B))
transpose_aux_in_agg(.(R, Rs), X1, .(C, Cs)) → U2_agg(R, Rs, X1, C, Cs, row2col_in_agaa(R, .(C, Cs), Cols1, Accm))
row2col_in_agaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_agaa(Xs, Cols, Cols1, As))
row2col_in_agaa([], [], [], []) → row2col_out_agaa([], [], [], [])
U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_agaa(Xs, Cols, Cols1, As)) → row2col_out_agaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As))
U2_agg(R, Rs, X1, C, Cs, row2col_out_agaa(R, .(C, Cs), Cols1, Accm)) → U3_agg(R, Rs, X1, C, Cs, transpose_aux_in_agg(Rs, Accm, Cols1))
transpose_aux_in_agg([], X, X) → transpose_aux_out_agg([], X, X)
U3_agg(R, Rs, X1, C, Cs, transpose_aux_out_agg(Rs, Accm, Cols1)) → transpose_aux_out_agg(.(R, Rs), X1, .(C, Cs))
U1_ag(A, B, transpose_aux_out_agg(A, [], B)) → transpose_out_ag(A, B)
TRANSPOSE_IN_AG(A, B) → U1_AG(A, B, transpose_aux_in_agg(A, [], B))
TRANSPOSE_IN_AG(A, B) → TRANSPOSE_AUX_IN_AGG(A, [], B)
TRANSPOSE_AUX_IN_AGG(.(R, Rs), X1, .(C, Cs)) → U2_AGG(R, Rs, X1, C, Cs, row2col_in_agaa(R, .(C, Cs), Cols1, Accm))
TRANSPOSE_AUX_IN_AGG(.(R, Rs), X1, .(C, Cs)) → ROW2COL_IN_AGAA(R, .(C, Cs), Cols1, Accm)
ROW2COL_IN_AGAA(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → U4_AGAA(X, Xs, Ys, Cols, Cols1, As, row2col_in_agaa(Xs, Cols, Cols1, As))
ROW2COL_IN_AGAA(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → ROW2COL_IN_AGAA(Xs, Cols, Cols1, As)
U2_AGG(R, Rs, X1, C, Cs, row2col_out_agaa(R, .(C, Cs), Cols1, Accm)) → U3_AGG(R, Rs, X1, C, Cs, transpose_aux_in_agg(Rs, Accm, Cols1))
U2_AGG(R, Rs, X1, C, Cs, row2col_out_agaa(R, .(C, Cs), Cols1, Accm)) → TRANSPOSE_AUX_IN_AGG(Rs, Accm, Cols1)
transpose_in_ag(A, B) → U1_ag(A, B, transpose_aux_in_agg(A, [], B))
transpose_aux_in_agg(.(R, Rs), X1, .(C, Cs)) → U2_agg(R, Rs, X1, C, Cs, row2col_in_agaa(R, .(C, Cs), Cols1, Accm))
row2col_in_agaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_agaa(Xs, Cols, Cols1, As))
row2col_in_agaa([], [], [], []) → row2col_out_agaa([], [], [], [])
U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_agaa(Xs, Cols, Cols1, As)) → row2col_out_agaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As))
U2_agg(R, Rs, X1, C, Cs, row2col_out_agaa(R, .(C, Cs), Cols1, Accm)) → U3_agg(R, Rs, X1, C, Cs, transpose_aux_in_agg(Rs, Accm, Cols1))
transpose_aux_in_agg([], X, X) → transpose_aux_out_agg([], X, X)
U3_agg(R, Rs, X1, C, Cs, transpose_aux_out_agg(Rs, Accm, Cols1)) → transpose_aux_out_agg(.(R, Rs), X1, .(C, Cs))
U1_ag(A, B, transpose_aux_out_agg(A, [], B)) → transpose_out_ag(A, B)
TRANSPOSE_IN_AG(A, B) → U1_AG(A, B, transpose_aux_in_agg(A, [], B))
TRANSPOSE_IN_AG(A, B) → TRANSPOSE_AUX_IN_AGG(A, [], B)
TRANSPOSE_AUX_IN_AGG(.(R, Rs), X1, .(C, Cs)) → U2_AGG(R, Rs, X1, C, Cs, row2col_in_agaa(R, .(C, Cs), Cols1, Accm))
TRANSPOSE_AUX_IN_AGG(.(R, Rs), X1, .(C, Cs)) → ROW2COL_IN_AGAA(R, .(C, Cs), Cols1, Accm)
ROW2COL_IN_AGAA(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → U4_AGAA(X, Xs, Ys, Cols, Cols1, As, row2col_in_agaa(Xs, Cols, Cols1, As))
ROW2COL_IN_AGAA(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → ROW2COL_IN_AGAA(Xs, Cols, Cols1, As)
U2_AGG(R, Rs, X1, C, Cs, row2col_out_agaa(R, .(C, Cs), Cols1, Accm)) → U3_AGG(R, Rs, X1, C, Cs, transpose_aux_in_agg(Rs, Accm, Cols1))
U2_AGG(R, Rs, X1, C, Cs, row2col_out_agaa(R, .(C, Cs), Cols1, Accm)) → TRANSPOSE_AUX_IN_AGG(Rs, Accm, Cols1)
transpose_in_ag(A, B) → U1_ag(A, B, transpose_aux_in_agg(A, [], B))
transpose_aux_in_agg(.(R, Rs), X1, .(C, Cs)) → U2_agg(R, Rs, X1, C, Cs, row2col_in_agaa(R, .(C, Cs), Cols1, Accm))
row2col_in_agaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_agaa(Xs, Cols, Cols1, As))
row2col_in_agaa([], [], [], []) → row2col_out_agaa([], [], [], [])
U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_agaa(Xs, Cols, Cols1, As)) → row2col_out_agaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As))
U2_agg(R, Rs, X1, C, Cs, row2col_out_agaa(R, .(C, Cs), Cols1, Accm)) → U3_agg(R, Rs, X1, C, Cs, transpose_aux_in_agg(Rs, Accm, Cols1))
transpose_aux_in_agg([], X, X) → transpose_aux_out_agg([], X, X)
U3_agg(R, Rs, X1, C, Cs, transpose_aux_out_agg(Rs, Accm, Cols1)) → transpose_aux_out_agg(.(R, Rs), X1, .(C, Cs))
U1_ag(A, B, transpose_aux_out_agg(A, [], B)) → transpose_out_ag(A, B)
ROW2COL_IN_AGAA(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → ROW2COL_IN_AGAA(Xs, Cols, Cols1, As)
transpose_in_ag(A, B) → U1_ag(A, B, transpose_aux_in_agg(A, [], B))
transpose_aux_in_agg(.(R, Rs), X1, .(C, Cs)) → U2_agg(R, Rs, X1, C, Cs, row2col_in_agaa(R, .(C, Cs), Cols1, Accm))
row2col_in_agaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_agaa(Xs, Cols, Cols1, As))
row2col_in_agaa([], [], [], []) → row2col_out_agaa([], [], [], [])
U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_agaa(Xs, Cols, Cols1, As)) → row2col_out_agaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As))
U2_agg(R, Rs, X1, C, Cs, row2col_out_agaa(R, .(C, Cs), Cols1, Accm)) → U3_agg(R, Rs, X1, C, Cs, transpose_aux_in_agg(Rs, Accm, Cols1))
transpose_aux_in_agg([], X, X) → transpose_aux_out_agg([], X, X)
U3_agg(R, Rs, X1, C, Cs, transpose_aux_out_agg(Rs, Accm, Cols1)) → transpose_aux_out_agg(.(R, Rs), X1, .(C, Cs))
U1_ag(A, B, transpose_aux_out_agg(A, [], B)) → transpose_out_ag(A, B)
ROW2COL_IN_AGAA(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → ROW2COL_IN_AGAA(Xs, Cols, Cols1, As)
ROW2COL_IN_AGAA(.(.(X, Ys), Cols)) → ROW2COL_IN_AGAA(Cols)
From the DPs we obtained the following set of size-change graphs:
U2_AGG(R, Rs, X1, C, Cs, row2col_out_agaa(R, .(C, Cs), Cols1, Accm)) → TRANSPOSE_AUX_IN_AGG(Rs, Accm, Cols1)
TRANSPOSE_AUX_IN_AGG(.(R, Rs), X1, .(C, Cs)) → U2_AGG(R, Rs, X1, C, Cs, row2col_in_agaa(R, .(C, Cs), Cols1, Accm))
transpose_in_ag(A, B) → U1_ag(A, B, transpose_aux_in_agg(A, [], B))
transpose_aux_in_agg(.(R, Rs), X1, .(C, Cs)) → U2_agg(R, Rs, X1, C, Cs, row2col_in_agaa(R, .(C, Cs), Cols1, Accm))
row2col_in_agaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_agaa(Xs, Cols, Cols1, As))
row2col_in_agaa([], [], [], []) → row2col_out_agaa([], [], [], [])
U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_agaa(Xs, Cols, Cols1, As)) → row2col_out_agaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As))
U2_agg(R, Rs, X1, C, Cs, row2col_out_agaa(R, .(C, Cs), Cols1, Accm)) → U3_agg(R, Rs, X1, C, Cs, transpose_aux_in_agg(Rs, Accm, Cols1))
transpose_aux_in_agg([], X, X) → transpose_aux_out_agg([], X, X)
U3_agg(R, Rs, X1, C, Cs, transpose_aux_out_agg(Rs, Accm, Cols1)) → transpose_aux_out_agg(.(R, Rs), X1, .(C, Cs))
U1_ag(A, B, transpose_aux_out_agg(A, [], B)) → transpose_out_ag(A, B)
U2_AGG(R, Rs, X1, C, Cs, row2col_out_agaa(R, .(C, Cs), Cols1, Accm)) → TRANSPOSE_AUX_IN_AGG(Rs, Accm, Cols1)
TRANSPOSE_AUX_IN_AGG(.(R, Rs), X1, .(C, Cs)) → U2_AGG(R, Rs, X1, C, Cs, row2col_in_agaa(R, .(C, Cs), Cols1, Accm))
row2col_in_agaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As)) → U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_in_agaa(Xs, Cols, Cols1, As))
U4_agaa(X, Xs, Ys, Cols, Cols1, As, row2col_out_agaa(Xs, Cols, Cols1, As)) → row2col_out_agaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As))
row2col_in_agaa([], [], [], []) → row2col_out_agaa([], [], [], [])
U2_AGG(X1, C, Cs, row2col_out_agaa(R, .(C, Cs), Cols1, Accm)) → TRANSPOSE_AUX_IN_AGG(Accm, Cols1)
TRANSPOSE_AUX_IN_AGG(X1, .(C, Cs)) → U2_AGG(X1, C, Cs, row2col_in_agaa(.(C, Cs)))
row2col_in_agaa(.(.(X, Ys), Cols)) → U4_agaa(X, Ys, Cols, row2col_in_agaa(Cols))
U4_agaa(X, Ys, Cols, row2col_out_agaa(Xs, Cols, Cols1, As)) → row2col_out_agaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As))
row2col_in_agaa([]) → row2col_out_agaa([], [], [], [])
row2col_in_agaa(x0)
U4_agaa(x0, x1, x2, x3)
row2col_in_agaa(.(.(X, Ys), Cols)) → U4_agaa(X, Ys, Cols, row2col_in_agaa(Cols))
POL(.(x1, x2)) = 1 + x1 + x2
POL(TRANSPOSE_AUX_IN_AGG(x1, x2)) = x2
POL(U2_AGG(x1, x2, x3, x4)) = x4
POL(U4_agaa(x1, x2, x3, x4)) = 1 + x2 + x4
POL([]) = 0
POL(row2col_in_agaa(x1)) = x1
POL(row2col_out_agaa(x1, x2, x3, x4)) = x3
U2_AGG(X1, C, Cs, row2col_out_agaa(R, .(C, Cs), Cols1, Accm)) → TRANSPOSE_AUX_IN_AGG(Accm, Cols1)
TRANSPOSE_AUX_IN_AGG(X1, .(C, Cs)) → U2_AGG(X1, C, Cs, row2col_in_agaa(.(C, Cs)))
U4_agaa(X, Ys, Cols, row2col_out_agaa(Xs, Cols, Cols1, As)) → row2col_out_agaa(.(X, Xs), .(.(X, Ys), Cols), .(Ys, Cols1), .([], As))
row2col_in_agaa([]) → row2col_out_agaa([], [], [], [])
row2col_in_agaa(x0)
U4_agaa(x0, x1, x2, x3)